Nuprl Lemma : select_append_front
11,40
postcript
pdf
T
:Type,
as
,
bs
:(
T
List),
i
:int_seg(0; ||
as
||). append(
as
;
bs
)[
i
] =
as
[
i
]
T
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Y
,
append(
as
;
bs
)
,
||
as
||
,
P
Q
,
P
Q
,
P
Q
,
False
,
P
Q
,
A
,
A
B
,
lelt(
i
;
j
;
k
)
,
int_seg(
i
;
j
)
,
P
Q
,
decidable(
P
)
,
prop{i:l}
Lemmas
length
wf1
,
int
seg
wf
,
decidable
int
equal
,
select
cons
hd
,
append
wf
,
select
cons
tl
,
length
append
,
non
neg
length
,
le
wf
origin
T:Type, as,bs:(T List), i:int_seg(0; ||as||). append(as; bs)[i] = as[i] 
T T:Type, as,bs:(T List), i:int_seg(0; ||as||). append(as; bs)[i] = as[i] T Tx:A. B(x)
Q
Q Q Q
A
B
Q